


 
#a,b,c,d,e,f,s0,s1,s2,s3,s4,s5  = definesymbols('a b c d e f 0 1 2 3 4 5')
#X = [s0,s1,s2,s3,s4,s5]
#sigma = [a,b,c,d,e,f]
#X0 = [s0]
#Xm = []
#sigmaobs = [a,b,c,d,e]
#trans = [[s0,f,s1],[s0,d,s5],[s0,e,s2],[s1,a,s3],[s2,a,s4],
#         [s3,e,s4],[s4,b,s0],[s5,c,s1]]
#
#
#G=fsa(X,sigma,trans,X0,Xm,Eobs = sigmaobs,name='$G$',type='plant') 


def dilatation(G,Sigmaisf):
    GA = G 
    for state in G.X:
        for event in (G.gamma(state) & set(Sigmaisf)):
            next_state = G.delta(state,event)
            event_uo = event + "'"
            GA = GA.addtransition([state,event_uo,next_state])   
    Gisf = observer(GA,G.E)
    Gisf.Eobs = G.Eobs
    Gisf.name = '$G_{isf}$ - intermitent failure model'          
    return Gisf
 
 
def sensormintopdown(G,sf,sigmaobs):
    curr_sensor = sigmaobs
    basis = []
    sensor_base = [curr_sensor]
    while sensor_base <> []:        
        curr_base = sensor_base.pop(0)
        curr_base.reverse()
        for event in curr_base:
            sigma_test = [x for x in curr_base if x<>event]
            sigma_test.sort()
            sigma_test.reverse()
            if sigma_test  ==[]: break
            if sigma_test not in basis:
                diag_test = verifymoreira(G,sf,sigma_test)
                if diag_test:
                    sensor_base.append(sigma_test)
                    basis.append(sigma_test)
    return basis



 ####[['a', 'b', 'c', 'd'], ['a', 'b', 'c', 'e'], ['a', 'c', 'd', 'e'], ['a', 'c', 'd'], ['a', 'b', 'c'], ['a', 'c', 'e'], ['a', 'c']]


def sensorbf(G,sf,sigmaobs):
    curr_sensor = sigmaobs    
    D0=diagnoser(G,sf,sigmaobs)
    diag_test, V0 = verifymoreira(G,sf,sigmaobs) 
    basis =[]
    result = [(sigmaobs,len(D0.X),D0.nxGraph.size(),len(V0.X),V0.nxGraph.size())]
    sensor_base = [curr_sensor]
    while sensor_base <> []:        
        curr_base = sensor_base.pop(0)
        curr_base.reverse()
        for event in curr_base:
            sigma_test = [x for x in curr_base if x<>event]
            sigma_test.sort()
            sigma_test.reverse()
            if sigma_test  ==[]: break
            if sigma_test not in basis:
                sensor_base.append(sigma_test)               
                diag_test, GV = verifymoreira(G,sf,sigma_test)   
                D = diagnoser(G,sf,sigma_test)  
                basis.append(sigma_test)
                result.append((sigma_test,len(D.X),D.nxGraph.size(),len(GV.X),GV.nxGraph.size(),diag_test))           
    return result



def entropy(G):
    graph = G.nxGraph  # the graph $$ is a living object
    adj_matrix = nx.to_numpy_matrix(graph)
    eigval,eigvec = linalg.eig(adj_matrix)
    abs_eigval = abs(eigval)
    maximum = abs_eigval.max()
    entropy = math.log(maximum,2)    
    return entropy


def diagnoser_entropy_analisys(G,sf,basis):
    table = []
    for event_set in basis:
        diag = diagnoser(G,sf,event_set)
        H_entr = entropy(diag)
        k = sensordelay(G,sf,event_set)
        k1 = sensordelay2(G,sf,event_set)
        table.append((event_set,H_entr,k,len(diag.X)))
    return table

def successor(V,GY,GN,statetuple):
        # through GY action
    failureset, k = statetuple 
    EMPTYSET=frozenset([])
    sigmaY=GY.E
    sigmaNY = GN.E - GY.E
    succY = EMPTYSET
    succNY = EMPTYSET
    
    for state in failureset:
        for edge in V.nxGraph.out_edges(state, keys=True):
            state = edge[0]
            next_state = edge[1]
            event = edge[2] 
            if next_state in V.Xm:
                if event in sigmaY:
                    succY = succY | frozenset([next_state])
                elif event in sigmaNY:
                    succNY = succNY | frozenset([next_state])            
    if succY == EMPTYSET:
        succ = frozenset([(succY,k),(succNY,k)])
    else:
        succ = frozenset([(succY,k+1),(succNY,k)])
    return succ

def sensordelay(G,sf,sigmaobs):
    GV, GY, GN = verifier(G,sf,sigmaobs)
    Y0=GV.Xm
    initial_set = (Y0,1)
    Y_curr= successor(GV,GY,GN,initial_set)
    Y_next=frozenset([])
    i=1
    while  (Y_next <> Y_curr) & (i<12):
        if i>1:
            Y_curr = Y_next
            Y_next = frozenset([])
        for element in Y_curr:
            Y_next = Y_next | successor(GV,GY,GN,element)
  
        i+=1
    delay=[]
    for state in Y_curr:
        delay.append(state[1])
    max_delay=    max(delay)
    return max_delay



#def sensordelay2(G,sf,sigmaobs):
#    GV, GY, GN = verifier(G,sf,sigmaobs)
#    sigmaY=GY.E
#    sigmaNY = GN.E - GY.E
#    graphver =  GV.nxGraph
#    graph_weight = nx.DiGraph()
#    for node in GV.Xm:
#        for edge in graphver.out_edges(node,keys=True):
#            next_node = edge[1]         
#            event = edge[2]                 
#            if event in sigmaY:
#                graph_weight.add_edge(node,next_node,weight=-1)
#            elif event in sigmaNY:    
#                graph_weight.add_edge(node,next_node,weight=0.0) 
#    delay=[]
#    for node in graph_weight.nodes_iter():
#        pred,distances = nx.bellman_ford(graph_weight,node)
#        delay.append(min(distances.values())) 
#    if delay ==[]: 
#        maxdelay = 1      
#    else:
#        maxdelay = abs(min(delay))+1                    
#    return  maxdelay



#example 1 ok bem logrado
#
#a,b,c,d,e,sf,g,x0,x1,x2,x3,x4,x5,x6,x7 = definesymbols('a b c d e f g 0 1 2 3 4 5 6 7')
#f=sf
#sigma=[a,b,c,d,e,sf]
#sigmaf=[sf]
#X=[x1,x2,x3,x4,x5,x6,x7]
#X0=[x1]
#Xm=[x1]
#trans=[[x1,c,x2],[x1,a,x5],[x2,sf,x3],[x3,e,x4],
#            [x4,d,x4],[x1,a,x5],[x5,b,x6],[x7,d,x7],[x3,a,x7],[x7,b,x1],[x4,b,x1],[x6,a,x4],[x4,b,x1],[x3,b,x1],[x6,b,x1]]
##sigmaobs1 = [a,b,c,d,e]
#sigmaobs = [a,b,c,d,e]
#G=fsa(X,sigma,trans,X0,Xm,Eobs=sigmaobs,name='$G$')  
#GV, GY, GN = verifier(G,sf,sigmaobs)

#import pylab as P # 
#nx.draw(g)  # networkx draw()
#P.show()    # pylab draw()
#draw(GV)

#basis = sensormintopdown(G,sf,sigmaobs)
#print sigmaobs
#table = diagnoser_entropy_analisys(G,sf,basis)
#for element in table:
#    print element


#d = diagnoser(G,sf,[a,c])
#e= entropy(d)
#print e

#example 2 muito bem too

#a,b,c,d,e,f,s0,s1,s2,s3,s4,s5  = definesymbols('a b c d e f 0 1 2 3 4 5')
#X = [s0,s1,s2,s3,s4,s5]
#sigma = [a,b,c,d,e,f]
#X0 = [s0]
#Xm = X0
#sigmaobs = [a,b,c,d,e]
#trans = [[s0,f,s1],[s0,d,s5],[s0,e,s2],[s1,a,s3],[s1,e,s3],[s2,a,s4],[s3,c,s1],[s3,b,s1],[s5,b,s3]]
#G=fsa(X,sigma,trans,X0,Xm,Eobs = sigmaobs,name='$G$',type='plant') 
#draw(G)
#basis = sensormintopdown(G,f,sigmaobs)
#table = diagnoser_entropy_analisys(G,f,basis)
#for element in table:
#    print element


#G_nondilated = fsa(X,sigma,trans,X0,Xm,Eobs =sigmanisf,name='$G$',type='plant') 
#G_dilated = dilatation(G,[b])
#basis1 = sensormintopdown(G_nondilated,f,sigmanisf)
#table1 = diagnoser_entropy_analisys(G_nondilated,f,basis1)
##table1 = diagnoser_entropy_analisys(G_nondilated,f,basis)
#d1 = diagnoser(G_nondilated,f,[a,c,d,e])
#ent = entropy(d1)
#print '[a,c,d,e]', ent
#for element in table1:
#   print element
#
#print '---------------'
#
#basis2 = sensormintopdown(G_dilated,f,sigmaobs)
#table2 = diagnoser_entropy_analisys(G_dilated,f,basis2)
#
#for element in table2:
#   print element
##basis2 = sensormintopdown(G_dilated,f,sigmaobs)
#draw(G,G_nondilated,G_dilated,)


# exemplo 3 I think this is the final example
a,b,c,d,sf,g,x0,x1,x2,x3,x4,x5,x6,x7 = definesymbols('a b c d  f g 0 1 2 3 4 5 6 7')
sigma= [a,b,c,d,sf]
X=[x1,x2,x3,x4,x5,x6,x7]
X0, Xm = [x1], [x1]

transicoes=[[x1,c,x2],[x1,a,x5],[x2,sf,x3],[x3,c,x4],[x4,a,x1],[x6,a,x1],[x6,c,x3],[x7,b,x1],
            [x4,d,x4],[x1,a,x5],[x5,b,x6],[x6,d,x6],[x7,d,x7],[x3,a,x7]]
sigmaobs = [a,b,c,d]
G=fsa(X,sigma,transicoes,X0,Xm,Eobs=sigmaobs,name='$G$') 
diag_test, GV = verifymoreira(G,sf,sigmaobs)
GV.set(name='Verifier Automaton $G_V$')
basis = sensorbf(G,sf,sigmaobs)

for eventset in basis:
    print eventset



